Suppose you have a function
add :: Int -> Int -> Int
add a b = a + b
Now suppose we have a second function
add5 :: Int -> Int
add5 x = add 5 x
So now add5 is a function that takes its argument, adds it to 5, and returns the result.
In Haskell, we can simplify the definition of add5 slightly by eliminating its argument, viz.:
add5 = add 5
This process is called "currying" (after Haskell Curry, who popularized the technique - yes, this is the same Haskell that the language is named after). add5 is now declared like a constant, but it is still a function with one argument.
Now instead of seeing add as a function that takes two arguments, we can see it is a function which takes one argument, and returns another function with the value 5 embedded inside it. This second function also takes one argument. When you call this second function with some argument, it adds the argument with the value that's embedded inside it (in this case, 5) and returns its result. So add x y can also be written (add x) y.
We can also write add5 like this:
add5 = \x -> add 5 x
An expression like \x -> y is a λ-expression. (The Greek letter lambda (λ) can't be typed on most keyboards, but \ looks a bit similar, so Haskell uses that instead.) It's an anonymous function that takes one argument, calling it x, and returns y. In lambda calculus notation, \x -> y is λx.y.
Suppose y is 5 + x. If we want to call our λ-expression \x -> 5 + x (in lambda calculus, λx.5 + x) with some value z, we write (\x -> 5 + x) z. (If this confuses you, notice that add 5 is just the same as \x -> 5 + x. I.e., it is a function that takes an argument and adds 5 to it. So (\x -> 5 + x) z is really just the same as (add 5) z, which as we established above is the same as add 5 z).
To evaluate (\x -> 5 + x) z, what we do is what is called a β-reduction (β being the Greek letter beta, if you didn't know). This basically involves replacing all occurences of the variable name x in the right hand side of the λ-expression with z. So (\x -> 5 + x) z becomes 5 + z. This is what is expressed on your notes as something like (λx.y) z => y[z/x] (I might have got the z and x the wrong way round here, since I don't have my notes handy right now). y[z/x], which some texts write y[x := z], just means y with all appearances of x replaced with z.
There are two more conversions you can do: α-conversion and η-conversion. η-conversion (η is called eta) is the name given to the process by which we derived the second definition of add5 from the first (and in reverse, yields the third from the second). Basically, an expression like \x -> f x can be replaced with just f, because this "application" function is just the same as the function that it applies. (Because for any z, (\x -> f x) z == f z.) However, to take an example from "The Haskell School of Expression" (again from memory), a function like foo x y = f y x y can't be replaced by foo x = f y x, because then what is y on the right? This is what the notes mean when they say that λx.f x can be replaced with f only if x doesn't appear free in f. (The meaning of "free" here will be explained in the next paragraph.)
α-conversion (α is called alpha) is really just a technicality of the textual nature of the lambda calculus, and it says that two expressions which differ only in the names of their variables are the same. For example, suppose we have a function \x -> (\x -> x). How then do we reduce (\x -> (\x -> x)) z? We can't reduce it to \x -> z, because the inner lambda declares x in the expression to the right of the arrow to be the function's argument (we say that this x is a bound variable, or is bound by this lambda - a free variable is simply one that isn't bound by a lambda). We have to rename this inner x to make it not clash. So we replace x in the inner lambda expression with some other name - say, y. Then \x -> x becomes \y -> y. Now (\x -> (\y -> y)) z obviously can only reduce to (\y -> y)[z/x], and since x doesn't appear in \y -> y, this reduces to just \y -> y.
So to summarise:
- λx.y means a function taking an argument x and returning y.
- λx.y is written in Haskell as \x -> y.
- In λx.f x, where x and f are variables, x is bound and f is free.
- A function taking multiple arguments is the same as a function taking one argument and returning a function taking another argument. So if foo bar baz = quux, then
foo bar baz = (foo bar) baz = (\x -> (\y -> quux)) bar baz = ((\x -> (\y -> quux)) bar) bazin which all of foo, foo bar, \x -> (\y -> quux), and (\x -> (\y -> quux)) bar are functions. Note that there is some syntactic sugar in Haskell:\x -> (\y -> quux) = \x -> \y -> quux = \x y -> quux - α-conversion: renaming bound variables, usually to avoid a clash.
- β-reduction: evaluating function applications.
- η-conversion: currying.